package controller.preprocessor;

import java.io.File;
import java.io.FileNotFoundException;
import java.io.IOException;
import java.io.RandomAccessFile;

import model.preprocessor.EPreProcessor;
import model.preprocessor.HypreParameter;
import model.preprocessor.PreProcessorParameter;
import model.preprocessor.PreProcessorResult;
import model.preprocessor.PreProcessorResultStatus;

/**
 * Implementation of preprocessor for hypre.
 * 
 * @author GRONOWSKI Stephane svan001@aol.com
 * 
 *         igsat 2010
 * 
 */
public class Hypre extends PreProcessorModel {
	public static final String	EXEC				= "hypre";
	public static final String	DESCRIPTION			= "Result of Hypre execution";

	public static final String	SAT_TOKEN			= "SATISFIABLE";
	public static final String	UNSATISFIABLE_TOKEN	= "UNSATISFIABLE";

	private HypreParameter		param;

	/**
	 * Create a Hypre preprocessor.
	 * 
	 * @param directory
	 *            directory where the executable file is.
	 * @throws IOException
	 *             if there is a problem with the file.
	 */
	public Hypre(File directory) throws IOException {
		super(DESCRIPTION, 0, -13, -14);
		param = new HypreParameter();
		type = EPreProcessor.HYPRE;
		if (!directory.isDirectory() || !new File(directory, EXEC).isFile())
			throw new IllegalArgumentException();

		try
		{
			path = directory.getCanonicalPath() + File.separator + EXEC;
		} catch (IOException e)
		{
			e.printStackTrace();
			throw new IOException();
		}
	}

	@Override
	public String[] getCommandLine(String cnfFile) {
		String[] tab = new String[4];

		// gere pas verbosity car hypre fais n'importe quoi
		// bash
		tab[0] = path;
		// bash
		tab[1] = "-o";
		// destination, fichier de sortie
		tab[2] = param.getOut();// correctFormatForLinux(param.getOut());
		// stdin
		tab[3] = cnfFile;// correctFormatForLinux(cnfFile);

		return tab;
	}

	@Override
	public boolean hasTimeout() {
		return false;
	}

	@Override
	protected void returnDefault(PreProcessorResult res) {
		getStdErr(res);

		// check the status vu que hypre le fait mal
		if (res.getStdin().indexOf(UNSATISFIABLE_TOKEN) != -1)
		{// status sat
			res.setStatus(PreProcessorResultStatus.UNSATISFIABLE);
			return;
		}

		if (res.getStdin().indexOf(SAT_TOKEN) != -1)
		{// status sat
			res.setStatus(PreProcessorResultStatus.SATISFIABLE);
			return;
		}

	}

	@Override
	protected void returnHasBeenStop(PreProcessorResult res) {
		getStdErr(res);
	}

	@Override
	protected void returnProblem(PreProcessorResult res) {
		getStdErr(res);
	}

	@Override
	protected void returnProblemCNF(PreProcessorResult res) {
		getStdErr(res);
	}

	@Override
	protected void returnUnSat(PreProcessorResult res) {
		getStdErr(res);
	}

	@Override
	protected void returnHasBeenTimeout(PreProcessorResult res) {
		getStdErr(res);
	}

	@Override
	public boolean checkParameter() {
		return param.basicCheck();
	}

	@Override
	public PreProcessorParameter getPreProcessorParameter() {
		return param;
	}

	/**
	 * 
	 * @return the hypre parameter.
	 */
	public HypreParameter getHypreParameter() {
		return param;
	}

	/*
	 * Get the information store in the preprocessor.dat file and delete it.
	 * 
	 * @param res the actual result
	 */
	private void getStdErr(PreProcessorResult res) {
		RandomAccessFile file;

		try
		{
			file = new RandomAccessFile("preprocessor.dat", "r");
		} catch (FileNotFoundException e)
		{
			return;
		}

		try
		{
			res.setStderr(file.readLine());
		} catch (IOException e)
		{
		}
		finally
		{
			File tmp = new File("preprocessor.dat");
			tmp.delete();
		}

	}

}
